Termination Proof Script

• Consider the SCC {13}. There are no usable rules. By taking the AF π with π(G) = 1 together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.


• Consider the SCC {9,11,12}. The usable rules are {5}. By taking the AF π with π(D) = π(e) = π(g) = 1 together with the lexicographic path order with empty precedence, the rules in {5,9,11} are weakly decreasing and rule 12 is strictly decreasing. There is one new SCC.
  • Consider the SCC {9,11}. By taking the AF π with π(e) = 1 and π(D) = 2 together with the lexicographic path order with empty precedence, rule 5 is weakly decreasing and the rules in {9,11} are strictly decreasing.


• Consider the SCC {6}. The usable rules are {2-5}. The constraints could not be solved.